perm filename ALPIG[EKL,SYS] blob
sn#864131 filedate 1988-08-04 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00011 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 first application: the case of alists
C00003 00003 PROOFS
C00004 00004 first application: to alists. Lemma:inj implies disjoint
C00007 00005 the sets in the sequence have positive multiplicity
C00010 00006 lemma mult_mult
C00012 00007 the main result for permutp: theorem permutp_injectp
C00017 00008 first application: to alists. Lemma:inj implies disjoint
C00020 00009 the sets in the sequence have positive multiplicity
C00023 00010 lemma mult_mult
C00025 00011 the main result for permutp: theorem permutp_injectp
C00030 ENDMK
C⊗;
;first application: the case of alists
(wipe-out)
(get-proofs pigeon prf ekl sys)
(proof alpig)
(axiom |∀u.inj(u)⊃disjoint(λm.mkset(nth(u,m)),length u)|)
(label inj_disj)
(axiom |∀u v.mklset u=mklset v⊃
(∀m.m<length u⊃1≤mult(v,mkset nth(u,m)))|)
(label permutp_injectp_lemma)
(axiom |∀u v.mklset u = mklset v ∧
(∀k.k<length u⊃mult(v,mkset nth(u,k))=1)⊃
(∀i.i<length v⊃mult(v,mkset nth(v,i))=1)|)
(label mult_mult)
(axiom |∀alist.permutp(alist)⊃injectp(alist)|)
(label theorem_permutp_injectp)
(save-proofs alpig)
;PROOFS
;first application: to alists. Lemma:inj implies disjoint
(wipe-out)
(get-proofs pigeon prf ekl sys)
(proof inj_disj)
;a main lemma for the induction step
1. (assume |inj u|)
(label injdsj0)
2. (rw * (open inj))
(label injdsj1)
;∀N M.N<LENGTH U∧M<LENGTH U∧NTH(U,N)=NTH(U,M)⊃N=M
3. (assume |n<length u|)
(label injdsj2)
4. (assume |(un(λm.mkset(nth(u,m)),n))(xv)∧(mkset(nth(u,n)))(xv)|)
(label injdsj3)
;need mksetfact
5. (ue ((u.u)(n.n)) mksetfact (open lesseq) injdsj2)
;UN(λM.MKSET(NTH(U,M)),N)=(λX.(∃K.K<N∧NTH(U,K)=X))
6. (rw injdsj3 (use * mode: exact) (open mkset) injdsj2)
;(∃K.K<N∧NTH(U,K)=XV)∧XV=NTH(U,N)
(label injdsj4)
7. (define kv |kv<n∧nth(u,kv)=xv| (use *))
(label injdsj5)
8. (derive |kv<length u∧nth(u,kv)=nth(u,n)| (* injdsj2 transitivity_of_order)
(use injdsj4 mode: always direction: reverse))
9. (derive |kv=n| (injdsj2 * injdsj1))
10. (rw injdsj5 (use * mode: exact) irreflexivity_of_order)
;FALSE
;deps: (INJDSJ0 INJDSJ3 INJDSJ2)
11. (ci injdsj3)
;¬((UN(λM.MKSET(NTH(U,M)),N))(XV)∧(MKSET(NTH(U,N)))(XV))
12. (ci (injdsj0 injdsj2))
;INJ(U)∧N<LENGTH U⊃¬((UN(λM.MKSET(NTH(U,M)),N))(XV)∧(MKSET(NTH(U,N)))(XV))
(label injdsj_lemma)
;the theorem follows
13. (ue (a |λn.inj(u)∧n≤length(u)⊃disjoint(λm.mkset nth(u,m),n)|) proof_by_induction
(open disjoint disj_pair intersection emptyp)
(use less_lesseqsucc mode: always direction: reverse)
(use injdsj_lemma mode: always)(part 1#2#1#1 (open lesseq)))
;∀N.INJ(U)∧N≤LENGTH U⊃DISJOINT(λM.MKSET(NTH(U,M)),N)
14. (ue (n |length u|) * (open lesseq))
;INJ(U)⊃DISJOINT(λM.MKSET(NTH(U,M)),LENGTH U)
;the sets in the sequence have positive multiplicity
(proof permutp_injectp_lemma)
1. (assume |mklset u=mklset v|)
(label pil1)
2. (assume |n<length u|)
(label pil2)
;use nthmember
3. (trw |nth(u,n)ε mklset u| (open epsilon mklset)
nthmember pil2)
;NTH(U,N)εMKLSET(U)
;deps: (PIL2)
;now use line pil1
4. (rw * (use pil1 mode: exact))
;NTH(U,N)εMKLSET(V)
;deps: (PIL1 PIL2)
;Finally, using MKLSET-FACT, we prove the existence of a kv such that
;nth(v,kv)=nth(u,n)
;labels: MKLSET_FACT
;(AXIOM |∀U.MKLSET(U)=(λX.(∃K.K<LENGTH U∧NTH(U,K)=X))|)
5. (rw * (use mklset_fact mode: exact) (open epsilon mkset))
;∃K.K<LENGTH V∧NTH(V,K)=NTH(U,N)
;deps: (PIL1 PIL2)
6. (define kv |kv<length(v)∧nth(v,kv)=nth(u,n)| *)
(label pil3)
;deps: (PIL1 PIL2)
7. (trw |member(nth(v,kv),v)| nthmember pil3)
;MEMBER(NTH(V,KV),V)
(label pil4)
;Therefore the set mkset(nth(u,n)) has positive multiplicity in v.
;labels: MEMBER_MULT
;(AXIOM |∀U Y A.MEMBER(Y,U)∧A(Y)⊃1≤MULT(U,A)|)
8. (ue ((u.v)(y.|nth(v,kv)|)(a.|mkset nth(u,n)|)) member_mult
(part 1(open mkset)) pil2 pil4 (use pil3 mode: always))
;1≤MULT(V,MKSET(NTH(U,N)))
;deps: (PIL1 PIL2)
9. (ci (pil1 pil2))
;MKLSET(U)=MKLSET(V)∧N<LENGTH U⊃1≤MULT(V,MKSET(NTH(U,N)))
;cosmetics
10. (derive |∀u v.mklset u=mklset v⊃(∀m.m<length u⊃1≤mult(v,mkset nth(u,m)))| *)
;lemma mult_mult
(proof mult_mult)
1. (assume |mklset u = mklset v|)
(label mm1)
2. (assume |∀m.m<length u ⊃ mult(v,mkset nth(u,m))=1|)
(label mm2)
3. (assume |i<length v|)
(label mm3)
4. (trw |nth(v,i) ε mklset v| (open epsilon mklset)
(use * nthmember mode: exact) )
;NTH(V,I)εMKLSET(V)
5. (rw * (use mm1 mode: exact direction: reverse))
;NTH(V,I)εMKLSET(U)
6. (rw * (use mklset_fact mode: exact) (open epsilon))
;∃K.K<LENGTH U∧NTH(U,K)=NTH(V,I)
7. (define mv |mv<length u ∧nth(u,mv)=nth(v,i)| *)
(label mm4)
;MV is unknown.
;the symbol MV is given the same declaration as M
;deps: (MM1 MM3)
8. (ue (m mv) mm2 (use * mode: always))
;MULT(V,MKSET(NTH(V,I)))=1
;deps: (MM1 MM2 MM3)
9. (ci mm3)
;I<LENGTH V⊃MULT(V,MKSET(NTH(V,I)))=1
;deps: (MM1 MM2)
10. (ci (mm1 mm2))
;MKLSET(U)=MKLSET(V)∧(∀M.M<LENGTH U⊃MULT(V,MKSET(NTH(U,M)))=1)⊃
;(I<LENGTH V⊃MULT(V,MKSET(NTH(V,I)))=1)
;the main result for permutp: theorem permutp_injectp
(proof permutp_injectp)
1. (assume |permutp alist|)
(label permutp_injectp1)
2. (rw * (open permutp))
;FUNCTP(ALIST)∧MKLSET(DOM(ALIST))=MKLSET(RANGE(ALIST))
(label permutp_injectp2)
3. (rw * (open functp))
;UNIQUENESS(DOM(ALIST))∧MKLSET(DOM(ALIST))=MKLSET(RANGE(ALIST))
(label permutp_injectp3)
;first step: disjointness of a suitable sequence of sets
;labels: UNIQUENESS_INJECTIVITY
;(AXIOM |∀U.UNIQUENESS(U)≡INJ(U)|)
;labels: INJ_DISJ
;(AXIOM |∀U.INJ(U)⊃DISJOINT(λM.MKSET(NTH(U,M)),LENGTH U)|)
4. (derive |inj(dom(alist))| (* uniqueness_injectivity))
;deps: (PERMUTP_INJECTP1)
5. (derive |disjoint(λm.mkset(nth(dom(alist),m)),length (dom(alist)))|
(* inj_disj))
(label permutp_injectp4)
;second step: multiplicity of the sets in the sequence is positive
;labels: PERMUTP_INJECTP_LEMMA
;(AXIOM
; |∀U V.MKLSET(U)=MKLSET(V)⊃(∀M.M<LENGTH U⊃1≤MULT(V,MKSET(NTH(U,M))))|)
6. (ue ((u.|dom alist|)(v.|range alist|)) permutp_injectp_lemma
(permutp_injectp3 permutp_injectp4))
;∀M.M<LENGTH (DOM(ALIST))⊃1≤MULT(RANGE(ALIST),MKSET(NTH(DOM(ALIST),M)))
(label permutp_injectp5)
;third step: application of the pigeon hole principle
;labels: PIGEONLIST
; (AXIOM
; |∀SETSEQ U.DISJOINT(SETSEQ,LENGTH U)∧(∀K.K<LENGTH U⊃1≤MULT(U,SETSEQ(K)))⊃
; (∀K.K<LENGTH U⊃1=MULT(U,SETSEQ(K)))|)
;need also
;labels: DOMRANGELENGTH
;(AXIOM |∀ALIST.LENGTH (DOM(ALIST))=LENGTH (RANGE(ALIST))|)
7. (ue ((setseq.|λm.mkset nth(dom alist,m)|)(u.|range alist|)) pigeonlist
(use domrangelength mode: exact direction: reverse)
permutp_injectp4 permutp_injectp5)
;∀K.K<LENGTH (DOM(ALIST))⊃1=MULT(RANGE(ALIST),MKSET(NTH(DOM(ALIST),K)))
;fourth step: injectivity
;labels: MULT_MULT
;∀U V.MKLSET(U)=MKLSET(V)∧(∀K.K<LENGTH U⊃MULT(V,MKSET(NTH(U,K)))=1)⊃
; (∀I.I<LENGTH V⊃MULT(V,MKSET(NTH(V,I)))=1)
8. (ue ((u.|dom(alist)|)(v.|range(alist)|)) mult_mult
permutp_injectp3 *)
;∀I.I<LENGTH (RANGE(ALIST))⊃MULT(RANGE(ALIST),MKSET(NTH(RANGE(ALIST),I)))=1
;deps: (PERMUTP_INJECTP1)
;apply mult_inj
;labels: MULT_INJ
;∀V.(∀K.K<LENGTH V⊃MULT(V,MKSET(NTH(V,K)))=1)⊃INJ(V)
9. (ue (v |range alist|) mult_inj *)
;INJ(RANGE(ALIST))
;deps: (PERMUTP_INJECTP1)
10. (derive |uniqueness(range alist)| (* uniqueness_injectivity))
;deps: (PERMUTP_INJECTP1)
11. (derive |injectp alist| (permutp_injectp2 *)(open injectp))
;deps: (PERMUTP_INJECTP1)
12. (ci (permutp_injectp1))
;PERMUTP(ALIST)⊃INJECTP(ALIST)
;first application: to alists. Lemma:inj implies disjoint
(wipe-out)
(get-proofs pigeon prf ekl sys)
(proof inj_disj)
;a main lemma for the induction step
1. (assume |inj u|)
(label injdsj0)
2. (rw * (open inj))
(label injdsj1)
;∀N M.N<LENGTH U∧M<LENGTH U∧NTH(U,N)=NTH(U,M)⊃N=M
3. (assume |n<length u|)
(label injdsj2)
4. (assume |(un(λm.mkset(nth(u,m)),n))(xv)∧(mkset(nth(u,n)))(xv)|)
(label injdsj3)
;need mksetfact
5. (ue ((u.u)(n.n)) mksetfact (open lesseq) injdsj2)
;UN(λM.MKSET(NTH(U,M)),N)=(λX.(∃K.K<N∧NTH(U,K)=X))
6. (rw injdsj3 (use * mode: exact) (open mkset) injdsj2)
;(∃K.K<N∧NTH(U,K)=XV)∧XV=NTH(U,N)
(label injdsj4)
7. (define kv |kv<n∧nth(u,kv)=xv| (use *))
(label injdsj5)
8. (derive |kv<length u∧nth(u,kv)=nth(u,n)| (* injdsj2 transitivity_of_order)
(use injdsj4 mode: always direction: reverse))
9. (derive |kv=n| (injdsj2 * injdsj1))
10. (rw injdsj5 (use * mode: exact) irreflexivity_of_order)
;FALSE
;deps: (INJDSJ0 INJDSJ3 INJDSJ2)
11. (ci injdsj3)
;¬((UN(λM.MKSET(NTH(U,M)),N))(XV)∧(MKSET(NTH(U,N)))(XV))
12. (ci (injdsj0 injdsj2))
;INJ(U)∧N<LENGTH U⊃¬((UN(λM.MKSET(NTH(U,M)),N))(XV)∧(MKSET(NTH(U,N)))(XV))
(label injdsj_lemma)
;the theorem follows
13. (ue (a |λn.inj(u)∧n≤length(u)⊃disjoint(λm.mkset nth(u,m),n)|) proof_by_induction
(open disjoint disj_pair intersection emptyp)
(use less_lesseqsucc mode: always direction: reverse)
(use injdsj_lemma mode: always)(part 1#2#1#1 (open lesseq)))
;∀N.INJ(U)∧N≤LENGTH U⊃DISJOINT(λM.MKSET(NTH(U,M)),N)
14. (ue (n |length u|) * (open lesseq))
;INJ(U)⊃DISJOINT(λM.MKSET(NTH(U,M)),LENGTH U)
;the sets in the sequence have positive multiplicity
(proof permutp_injectp_lemma)
1. (assume |mklset u=mklset v|)
(label pil1)
2. (assume |n<length u|)
(label pil2)
;use nthmember
3. (trw |nth(u,n)ε mklset u| (open epsilon mklset)
nthmember pil2)
;NTH(U,N)εMKLSET(U)
;deps: (PIL2)
;now use line pil1
4. (rw * (use pil1 mode: exact))
;NTH(U,N)εMKLSET(V)
;deps: (PIL1 PIL2)
;Finally, using MKLSET-FACT, we prove the existence of a kv such that
;nth(v,kv)=nth(u,n)
;labels: MKLSET_FACT
;(AXIOM |∀U.MKLSET(U)=(λX.(∃K.K<LENGTH U∧NTH(U,K)=X))|)
5. (rw * (use mklset_fact mode: exact) (open epsilon mkset))
;∃K.K<LENGTH V∧NTH(V,K)=NTH(U,N)
;deps: (PIL1 PIL2)
6. (define kv |kv<length(v)∧nth(v,kv)=nth(u,n)| *)
(label pil3)
;deps: (PIL1 PIL2)
7. (trw |member(nth(v,kv),v)| nthmember pil3)
;MEMBER(NTH(V,KV),V)
(label pil4)
;Therefore the set mkset(nth(u,n)) has positive multiplicity in v.
;labels: MEMBER_MULT
;(AXIOM |∀U Y A.MEMBER(Y,U)∧A(Y)⊃1≤MULT(U,A)|)
8. (ue ((u.v)(y.|nth(v,kv)|)(a.|mkset nth(u,n)|)) member_mult
(part 1(open mkset)) pil2 pil4 (use pil3 mode: always))
;1≤MULT(V,MKSET(NTH(U,N)))
;deps: (PIL1 PIL2)
9. (ci (pil1 pil2))
;MKLSET(U)=MKLSET(V)∧N<LENGTH U⊃1≤MULT(V,MKSET(NTH(U,N)))
;cosmetics
10. (derive |∀u v.mklset u=mklset v⊃(∀m.m<length u⊃1≤mult(v,mkset nth(u,m)))| *)
;lemma mult_mult
(proof mult_mult)
1. (assume |mklset u = mklset v|)
(label mm1)
2. (assume |∀m.m<length u ⊃ mult(v,mkset nth(u,m))=1|)
(label mm2)
3. (assume |i<length v|)
(label mm3)
4. (trw |nth(v,i) ε mklset v| (open epsilon mklset)
(use * nthmember mode: exact) )
;NTH(V,I)εMKLSET(V)
5. (rw * (use mm1 mode: exact direction: reverse))
;NTH(V,I)εMKLSET(U)
6. (rw * (use mklset_fact mode: exact) (open epsilon))
;∃K.K<LENGTH U∧NTH(U,K)=NTH(V,I)
7. (define mv |mv<length u ∧nth(u,mv)=nth(v,i)| *)
(label mm4)
;MV is unknown.
;the symbol MV is given the same declaration as M
;deps: (MM1 MM3)
8. (ue (m mv) mm2 (use * mode: always))
;MULT(V,MKSET(NTH(V,I)))=1
;deps: (MM1 MM2 MM3)
9. (ci mm3)
;I<LENGTH V⊃MULT(V,MKSET(NTH(V,I)))=1
;deps: (MM1 MM2)
10. (ci (mm1 mm2))
;MKLSET(U)=MKLSET(V)∧(∀M.M<LENGTH U⊃MULT(V,MKSET(NTH(U,M)))=1)⊃
;(I<LENGTH V⊃MULT(V,MKSET(NTH(V,I)))=1)
;the main result for permutp: theorem permutp_injectp
(proof permutp_injectp)
1. (assume |permutp alist|)
(label permutp_injectp1)
2. (rw * (open permutp))
;FUNCTP(ALIST)∧MKLSET(DOM(ALIST))=MKLSET(RANGE(ALIST))
(label permutp_injectp2)
3. (rw * (open functp))
;UNIQUENESS(DOM(ALIST))∧MKLSET(DOM(ALIST))=MKLSET(RANGE(ALIST))
(label permutp_injectp3)
;first step: disjointness of a suitable sequence of sets
;labels: UNIQUENESS_INJECTIVITY
;(AXIOM |∀U.UNIQUENESS(U)≡INJ(U)|)
;labels: INJ_DISJ
;(AXIOM |∀U.INJ(U)⊃DISJOINT(λM.MKSET(NTH(U,M)),LENGTH U)|)
4. (derive |inj(dom(alist))| (* uniqueness_injectivity))
;deps: (PERMUTP_INJECTP1)
5. (derive |disjoint(λm.mkset(nth(dom(alist),m)),length (dom(alist)))|
(* inj_disj))
(label permutp_injectp4)
;second step: multiplicity of the sets in the sequence is positive
;labels: PERMUTP_INJECTP_LEMMA
;(AXIOM
; |∀U V.MKLSET(U)=MKLSET(V)⊃(∀M.M<LENGTH U⊃1≤MULT(V,MKSET(NTH(U,M))))|)
6. (ue ((u.|dom alist|)(v.|range alist|)) permutp_injectp_lemma
(permutp_injectp3 permutp_injectp4))
;∀M.M<LENGTH (DOM(ALIST))⊃1≤MULT(RANGE(ALIST),MKSET(NTH(DOM(ALIST),M)))
(label permutp_injectp5)
;third step: application of the pigeon hole principle
;labels: PIGEONLIST
; (AXIOM
; |∀SETSEQ U.DISJOINT(SETSEQ,LENGTH U)∧(∀K.K<LENGTH U⊃1≤MULT(U,SETSEQ(K)))⊃
; (∀K.K<LENGTH U⊃1=MULT(U,SETSEQ(K)))|)
;need also
;labels: DOMRANGELENGTH
;(AXIOM |∀ALIST.LENGTH (DOM(ALIST))=LENGTH (RANGE(ALIST))|)
7. (ue ((setseq.|λm.mkset nth(dom alist,m)|)(u.|range alist|)) pigeonlist
(use domrangelength mode: exact direction: reverse)
permutp_injectp4 permutp_injectp5)
;∀K.K<LENGTH (DOM(ALIST))⊃1=MULT(RANGE(ALIST),MKSET(NTH(DOM(ALIST),K)))
;fourth step: injectivity
;labels: MULT_MULT
;∀U V.MKLSET(U)=MKLSET(V)∧(∀K.K<LENGTH U⊃MULT(V,MKSET(NTH(U,K)))=1)⊃
; (∀I.I<LENGTH V⊃MULT(V,MKSET(NTH(V,I)))=1)
8. (ue ((u.|dom(alist)|)(v.|range(alist)|)) mult_mult
permutp_injectp3 *)
;∀I.I<LENGTH (RANGE(ALIST))⊃MULT(RANGE(ALIST),MKSET(NTH(RANGE(ALIST),I)))=1
;deps: (PERMUTP_INJECTP1)
;apply mult_inj
;labels: MULT_INJ
;∀V.(∀K.K<LENGTH V⊃MULT(V,MKSET(NTH(V,K)))=1)⊃INJ(V)
9. (ue (v |range alist|) mult_inj *)
;INJ(RANGE(ALIST))
;deps: (PERMUTP_INJECTP1)
10. (derive |uniqueness(range alist)| (* uniqueness_injectivity))
;deps: (PERMUTP_INJECTP1)
11. (derive |injectp alist| (permutp_injectp2 *)(open injectp))
;deps: (PERMUTP_INJECTP1)
12. (ci (permutp_injectp1))
;PERMUTP(ALIST)⊃INJECTP(ALIST)